lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

Weak head normal form.md (387B)

      1 +++
      2 title = "Weak head normal form"
      3 +++
      4 
      5 # Weak head normal form
      6 WHNF: at least one symbol is stable under reduction (the top part)
      7 
      8 If the root is an abstraction, or applications with a variable on the left, it’s in WHNF.
      9 
     10 every normal form is a WHNF, not necessarily the other way around.
     11 
     12 definition: λx.P, xP₁...Pn
     13 
     14 examples: x, λx.x, xΩ, λx.Ω
     15 
     16 lazy reduction: stop at WHNF